Inference at * 
Iof proof for Lemma zip wf:


  T1, T2:Type, as:(T1 List), bs:(T2 List). zip(as;bs)  ((:T1  T2) List) 

latex

 by ((((((((((((((((((((((((D 0) 
CollapseTHENM (D 0))) 
CollapseTHENM (D 0))) 

CoCollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C) inil_term)))) 
CollapseTHEN (ListInd (-1)))) 
CollapseTHEN (RecUnfold `zip` 0))) 

CoCollapseTHEN (Reduce 0))) 
CollapseTHEN (Try (Complete (Auto_aux (first_nat 1:n) ((first_nat 
C1:n),(first_nat 1000:n)) (first_tok :t) inil_term))))) 
CollapseTHEN (D 0))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))) 

C(CollapseTHEN (ListInd (-1)))) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN ((Auto_aux (first_nat 
C1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: .....subterm..... T:t2:n

C1: 1. T1 : Type
C1: 2. T2 : Type
C1: 3. T1 List
C1: 4. u : T1
C1: 5. v : T1 List
C1: 6. bs:(T2 List). zip(v;bs)  ((:T1  T2) List)
C1: 7. T2 List
C1: 8. T2
C1: 9. v1 : T2 List
C1: 10. rec-case(v1) of [] => [] | b::bs' => .[<u, b> / zip(v;bs')]  ((:T1  T2) List)
C1:   zip(v;v1)  ((:T1  T2) List)
C.

Definitions	Y, zip(as;bs), t  T, x:A. B(x)
Lemmas	member wf